$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), $f$:($T$$\rightarrow$$T$).
\\[0ex]retraction($T$;$f$) $\Rightarrow$ ($\forall$$x$:$T$. $f$($f$$\ast\ast$($x$)) = $f$$\ast\ast$($x$) \& $f$$\ast\ast$($x$) is $f$$\ast$($x$))